Refactored the define attribute on functions #236
Conversation
Instead of pushing definitions through encoded as axioms, now there is a list of definitions that gets processed separately from axioms.
Also added two more regressions.
When function definition body is walked over to turn it into SMT format, variables are being picked up and subsequently declared. We should avoid this since they are in fact function arguments and hence do not need declarations.
|
Ok, I think this is ready for a round of reviewing. |
Dependencies found in function definitions were printed after the definitions themselves in the generated VCs, which led to missing declaration errors. I am now flushing dependencies before printing function definitions.
|
@RustanLeino Any chance you could also review it before it gets merged? Thanks! |
I added the same option to the function inline version when I updated Z3.
As for now, I haven't managed to get it to work with polymorphic functions. This is a TODO for future work.
Currently definition of polymorphic functions is not supported.
| // the body is only set if the function is declared with {:inline} | ||
| public Expr Body; | ||
| public Expr Body; // Only set if the function is declared with {:inline} | ||
| public NAryExpr DefinitionBody; // Only set if the function is declared with {:define} |
There was a problem hiding this comment.
I concede that this makes the code clearer, but it does require you to duplicate code - wherever Body was used before, there are now two cases. I did not attempt to check that you caught every such case, so I have to trust you did.
There was a problem hiding this comment.
Yes, you are absolutely right, and this is a valid point. I made sure I checked off all such occurrences and I don't think I missed any.
The original plan I discussed with Shaz was not to duplicate code, but to use Body for both. However, Body is being leveraged in rarely used codes (AbstractHoudini and FixedPointVC) that we do not quite understand. Hence, I was hesitant to reuse it until someone either cleans up AbstractHoudini and FixedPointVC or completely removes them. My time was running out and I did not get to that.
This feature was introduced recently in Boogie/Corral and it would be good to leverage it if it does not affect the performance and causes a major slow-down. See: boogie-org/boogie#236
This pull request continues where #196 left off. In particular, instead of pushing function definitions through Boogie by piggybacking on axioms, I refactored this part to instead have an explicit list of function definitions.